Add solver independent quantifier elimination with ultimate eliminator #462
Conversation
format code add missing UltimateEliminator dependencies
…k most solvers (now 152 tests run over all solvers compared to 89 before)
…bles for quantifiers
|
@kfriedberger @PhilippWendler we have 3 warnings from Spotbugs that are empty in this PR. Do you happen to know the reason for this or how to find out? |
|
Please check the code for unused fields or variables. I also would like to have better Spotbugs messages. I assume this topic is more general and applies to more project at SoSy-Lab. I have not yet checked in CPAchecker or VCloud, whether SpotBugs prints so minimal errors there, too. UPDATE: TODO: |
|
Thanks for the help! |
This is a known SpotBugs bug and fixed in version 4.9.0 (from January). |
…verride it in Mathsat5QuantifiedFormulaManager
…antifierCreationMethod
…r_elimination_with_ultimate_eliminator' into add_solver_independent_quantifier_elimination_with_ultimate_eliminator # Conflicts: # src/org/sosy_lab/java_smt/delegate/debugging/DebuggingQuantifiedFormulaManager.java # src/org/sosy_lab/java_smt/delegate/statistics/StatisticsQuantifiedFormulaManager.java # src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedQuantifiedFormulaManager.java
There was a problem hiding this comment.
Your test classes test the options for quantifier creation and elimination explicitly. However, you could add a second or even third parameter to the parameterized test setup of SolverBasedTest0.ParameterizedSolverBasedTest0 (by extending it with a subclass or two). Then you could automatically check ALL option combinations with all solvers.
Also, please extend the documentation of the methods in the AbstractQuantifiedFormulaManager that deal with the interaction of UE with the solvers. They have very little to none currently.
| return fmgr.orElseThrow(); | ||
| } | ||
|
|
||
| public void setFmgr(AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> pFmgr) { |
There was a problem hiding this comment.
Why not simply set it in the AbstractFormulaManagers constructor for existing QuantifiedFormulaManagers?
Then its in the same package and can be package-private.
This would also prevent other developers from forgetting.
| @Override | ||
| protected String dumpFormula(BooleanFormula bf) { | ||
| return ((Mathsat5FormulaManager) getFmgr()) | ||
| .dumpFormulaImplExt(extractInfo(bf), "qFormulaNameMathsat5"); |
There was a problem hiding this comment.
Why not out the implementation of dumpFormulaImplExt here?
| @@ -39,14 +45,23 @@ public UltimateEliminatorWrapper(LogManager pLog) { | |||
| log = pLog; | |||
| } | |||
|
|
|||
| /* | |||
| * Simplifies and try to remove the quantifiers from the given term using the UltimateEliminator. | |||
| */ | |||
| public Term simplify(Term pTerm) { | |||
| return ultimateEliminator.simplify(pTerm); | |||
There was a problem hiding this comment.
UE has lots of options that allow different types of simplifications.
Do we have a way of changing those?
There was a problem hiding this comment.
As far as I understand it, we currently do not. As we would have to Override the "simplify" method in the UltimateEliminator source code to do so. I tried creating a class that extends UltimateEliminator to override the method, however, it ended with accessibility issues
See: https://github.com/ultimate-pa/ultimate/blob/0ed21c286de111155dccfbaf80bfbc5906a6435f/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/UltimateEliminator.java#L268
| return wrap(eliminateQuantifiers(extractInfo(pF))); | ||
| } else { | ||
| } catch (Exception e1) { |
There was a problem hiding this comment.
Please never plainly catch Exception. Always catch named exceptions only.
| } | ||
|
|
||
| case ULTIMATE_ELIMINATOR_FALLBACK_ON_FAILURE: | ||
| try { |
There was a problem hiding this comment.
You are repeating the try-catch blocks quite a lot. You could extract them into a method.
add Level.WARNING instead of null to logger
(To get the right formula information: with visitor get the name and type of bound variables)